COMMENT ā VALID 00002 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 Oct 30, 1980 C00003 ENDMK Cā; Oct 30, 1980 two additional chapters. proof methods for impure and unclean programs transformations of programs, perhaps proofs of macros got tangled proving properties of u ⤠v as predicate and as function.